/*
 * $Id: JPFCheckerSearch.java 2233 2007-04-18 14:49:48Z kofron $
 *
 * Behavior Protocols extensions for static and runtime checking
 * developed for the Julia implementation of Fractal.
 *
 * Copyright (C) 2006
 *    Formal Methods In Software Engineering Group
 *    Institute of Computer Science
 *    Academy of Sciences of the Czech Republic
 *
 * Copyright (C) 2006 France Telecom
 *
 * This library is free software; you can redistribute it and/or
 * modify it under the terms of the GNU Lesser General Public
 * License as published by the Free Software Foundation; either
 * version 2 of the License, or (at your option) any later version.
 *
 * This library is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 * Lesser General Public License for more details.
 *
 * You should have received a copy of the GNU Lesser General Public
 * License along with this library; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307 USA
 *
 * Contact: ft@nenya.ms.mff.cuni.cz
 * Authors: Pavel Parizek <parizek@nenya.ms.mff.cuni.cz>
 * 
 */
package org.objectweb.fractal.bpc.jpf;

import gov.nasa.jpf.Config;
import gov.nasa.jpf.jvm.JVM;
import gov.nasa.jpf.search.Search;

import org.objectweb.fractal.bpc.checker.DFSR.JPFTraverser;


/**
 * Modified version of the DFSearch class distributed with JPF.
 */
public class JPFCheckerSearch extends Search 
{
  private JPFTraverser traverser = null;
  
  public JPFCheckerSearch (Config config, JVM vm) 
  {
  	super(config, vm);
  }
  
  public boolean requestBacktrack () 
  {
    doBacktrack = true;
    
    return true;
  }
  
  public void setJPFTraverser(JPFTraverser jt)
  {
      this.traverser = jt;
  }
  
  /**
   * Extended version of the search method from the DFSearch class that supports coordination of backtracking.
   */
  public void search () 
  {
    int maxDepth = getMaxSearchDepth();
    
    depth = 0;
    notifySearchStarted();
    
    while (!done) 
    {
	  //System.err.println("JPFCheckerSearch: stateId = "+vm.getSystemState().getId()+", isNewState = "+isNewState+", wants.backtrack = "+traverser.wantsBacktrack()+", isEndState = "+isEndState);
	  if ( (!isNewState && traverser.wantsBacktrack()) || isEndState ) 
      {
        if (!backtrack()) break; // backtrack not possible, done
        
        depth--;
        notifyStateBacktracked();
      }

      if (forward()) 
      {        
        notifyStateAdvanced();
        
        if (hasPropertyTermination()) break;
        
          depth++;
                    
          if (depth >= maxDepth) 
          {
            isEndState = true;
            notifySearchConstraintHit(QUEUE_CONSTRAINT);
          }
          
          /*
          if (!checkStateSpaceLimit()) 
          {
            notifySearchConstraintHit(SIZE_CONSTRAINT);
            // can't go on, we exhausted our memory
            break;
          }
          */
      } 
      else 
      { 
          // state was processed
        notifyStateProcessed();
      }
    }
    
    notifySearchFinished();
    
    /* PP */
    hasPropertyTermination();
  }
  
  
  public boolean supportsBacktrack () 
  {
    return true;
  }
}
